/* Bogor: An Extensible and Highly-Modular Model Checking Framework
 * Copyright (c) 2002-2005 Kansas State University
 *
 * This software is licensed using the SAnToS Laboratory Open Academic License.
 * You should have received a copy of the License in the top directory of this
 * software distribution package. If not, then write to
 * SAnToS Laboratory, 234 Nichols Hall, Manhattan, KS 66506, USA.
 *
 * The SAnToS Laboratory homepage is located at http://www.cis.ksu.edu/santos.
 * The Bogor homepage is located at http://bogor.projects.cis.ksu.edu.
 */


import java.io.PrintWriter;
import java.text.DecimalFormat;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.Collection;
import java.util.Iterator;
import java.util.List;
import java.util.ListIterator;
import java.util.Map;
import java.util.Properties;

import edu.ksu.cis.projects.bogor.IBogorConfiguration;
import edu.ksu.cis.projects.bogor.ast.Action;
import edu.ksu.cis.projects.bogor.ast.BlockTransformation;
import edu.ksu.cis.projects.bogor.ast.Exp;
import edu.ksu.cis.projects.bogor.ast.FSM;
import edu.ksu.cis.projects.bogor.ast.Global;
import edu.ksu.cis.projects.bogor.ast.InitialValue;
import edu.ksu.cis.projects.bogor.ast.InvokeTransformation;
import edu.ksu.cis.projects.bogor.ast.Local;
import edu.ksu.cis.projects.bogor.ast.Location;
import edu.ksu.cis.projects.bogor.ast.Transformation;
import edu.ksu.cis.projects.bogor.ast.Visibility;
import edu.ksu.cis.projects.bogor.ast.checker.ConstIntExpEvaluator;
import edu.ksu.cis.projects.bogor.module.ConfigurationMessages;
import edu.ksu.cis.projects.bogor.module.DefaultCounterExampleSchedulingInfo;
import edu.ksu.cis.projects.bogor.module.DefaultMessageStore;
import edu.ksu.cis.projects.bogor.module.IActionTaker;
import edu.ksu.cis.projects.bogor.module.IBacktrackingInfoFactory;
import edu.ksu.cis.projects.bogor.module.ICounterExampleSchedulingInfo;
import edu.ksu.cis.projects.bogor.module.ICounterExampleWriter;
import edu.ksu.cis.projects.bogor.module.IEnabledTransformationsContext;
import edu.ksu.cis.projects.bogor.module.IExpEvaluator;
import edu.ksu.cis.projects.bogor.module.IMessageStore;
import edu.ksu.cis.projects.bogor.module.IProgressManager;
import edu.ksu.cis.projects.bogor.module.ISchedulingStrategist;
import edu.ksu.cis.projects.bogor.module.ISchedulingStrategyContext;
import edu.ksu.cis.projects.bogor.module.ISchedulingStrategyInfo;
import edu.ksu.cis.projects.bogor.module.ISearcher;
import edu.ksu.cis.projects.bogor.module.IStateFactory;
import edu.ksu.cis.projects.bogor.module.IStateFactoryArguments;
import edu.ksu.cis.projects.bogor.module.IStateManager;
import edu.ksu.cis.projects.bogor.module.IStoreStateResult;
import edu.ksu.cis.projects.bogor.module.ITransformer;
import edu.ksu.cis.projects.bogor.module.IValueFactory;
import edu.ksu.cis.projects.bogor.module.backtrack.IActionBacktrackingInfo;
import edu.ksu.cis.projects.bogor.module.backtrack.IBacktrackingInfo;
import edu.ksu.cis.projects.bogor.module.backtrack.IEndStateBacktrackingInfo;
import edu.ksu.cis.projects.bogor.module.backtrack.IExceptionBacktrackingInfo;
import edu.ksu.cis.projects.bogor.module.backtrack.INextStateBacktrackingInfo;
import edu.ksu.cis.projects.bogor.module.backtrack.IPostNextStateBacktrackingInfo;
import edu.ksu.cis.projects.bogor.module.backtrack.ITransformationBacktrackingInfo;
import edu.ksu.cis.projects.bogor.module.config.Domain;
import edu.ksu.cis.projects.bogor.module.config.ISelfDescribingModule;
import edu.ksu.cis.projects.bogor.module.config.OptionScope;
import edu.ksu.cis.projects.bogor.module.state.IState;
import edu.ksu.cis.projects.bogor.module.throwable.ArithmeticBogorException;
import edu.ksu.cis.projects.bogor.module.throwable.AssertionBogorException;
import edu.ksu.cis.projects.bogor.module.throwable.BadMonitorBogorException;
import edu.ksu.cis.projects.bogor.module.throwable.BogorException;
import edu.ksu.cis.projects.bogor.module.throwable.CastBogorException;
import edu.ksu.cis.projects.bogor.module.throwable.ExceptionThrownBogorException;
import edu.ksu.cis.projects.bogor.module.throwable.ExtFailedBogorException;
import edu.ksu.cis.projects.bogor.module.throwable.IllFormedModelBogorException;
import edu.ksu.cis.projects.bogor.module.throwable.IndexOutOfBoundsBogorException;
import edu.ksu.cis.projects.bogor.module.throwable.NullPointerBogorException;
import edu.ksu.cis.projects.bogor.module.throwable.RangeBogorException;
import edu.ksu.cis.projects.bogor.module.value.IIntValue;
import edu.ksu.cis.projects.bogor.module.value.IValue;
import edu.ksu.cis.projects.bogor.module.value.IValueArray;
import edu.ksu.cis.projects.bogor.symboltable.FSMSymbolTable;
import edu.ksu.cis.projects.bogor.symboltable.SymbolTable;
import edu.ksu.cis.projects.bogor.type.BooleanType;
import edu.ksu.cis.projects.bogor.type.FunType;
import edu.ksu.cis.projects.bogor.type.Type;
import edu.ksu.cis.projects.bogor.util.FileMessage;
import edu.ksu.cis.projects.bogor.util.Pair;
import edu.ksu.cis.projects.bogor.util.Triple;
import edu.ksu.cis.projects.bogor.util.Util;
import edu.ksu.cis.projects.trove.custom.IntIntTable;
import edu.ksu.cis.projects.trove.custom.IntList;
import edu.ksu.cis.projects.trove.custom.IntObjectTable;

/**
 * @author <a href="mailto:robby@cis.ksu.edu">Robby </a>
 * @author <a href="mailto:matt@cis.ksu.edu">Matt Hoosier </a>
 * @version CVS $Revision: 1.86 $ $Date: 2005/08/15 20:27:48 $
 */
public class MyDefaultSearcher
    implements ISearcher, ISelfDescribingModule
{
    // ~ Static variables/initializers
    // ..........................................

    protected static final String PRINT_VERBOSE_TRACE_ID = "printVerboseTrace";

    protected static final String PRINT_STATUS_ID = "printStatus";

    protected static final String TRAIL_EXT = "bogor-trails";

    protected static final String PRINT_COUNTER_EXAMPLES_ID = "printCounterExamples";

    protected static final String WRITE_TRAIL_FILE_ID = "writeTrailFile";

    protected static final String ALL_AS_ERRORS_ID = "allAsErrors";

    protected static final String MAX_ERRORS_ID = "maxErrors";

    protected static final String MAX_DEPTH_ID = "maxDepth";

    protected static final String MAX_INVISIBLE_MOVES_ID = "maxInvisibleMoves";

    protected static final String UPDATE_STATE_INCREMENT_ID = "updateStateIncrement";

    protected static final String UPDATE_TRANSITION_INCREMENT_ID = "updateTransitionIncrement";

    protected static final String INVARIANTS_ID = "invariants";

    protected static final String CHECK_BACKTRACK_ID = "checkBacktrack";

    // ~ Instance variables
    // .....................................................

    protected boolean printCounterExamples = false;

    protected boolean writeTrailFile = true;

    protected boolean allAsErrors = false;

    protected boolean printVerboseTrace = true;

    protected boolean printStatus = true;

    // note: currently does not support extension
    protected int maxErrors = 0;

    protected int maxDepth = Integer.MAX_VALUE >> 1;

    protected int updateStateIncrement = 10000;

    protected int maxInvisibleMoves = Integer.MAX_VALUE >> 1;

    protected long updateTransitionIncrement = 10000;

    protected boolean checkBacktrack = false;

    protected String[] invariants;

    protected PrintWriter pw;

    /**
     * @uml.property name="backtrackingInfos"
     */
    protected ArrayList<ITransformationBacktrackingInfo> backtrackingInfos;

    protected IBogorConfiguration bc;

    protected IActionTaker at;

    protected IBacktrackingInfoFactory bif;

    protected ICounterExampleWriter cew;

    protected IExpEvaluator ee;

    protected ISchedulingStrategist ss;

    /**
     * @uml.property name="state"
     */
    protected IState state;

    protected IStateFactory sf;

    protected IStateManager sm;

    protected ISearcher sr;

    protected ITransformer tr;

    protected IValueFactory vf;

    protected IProgressManager pm;

    protected SymbolTable symbolTable;

    protected boolean isInvisible;

    protected boolean seenState;

    protected int lastMovedThreadId;

    protected int stateId;

    protected int invisibleMoves;

    protected int currentDepth;

    protected int currentMaxDepth;

    protected int errors;

    protected int seenStates;

    protected long startTime;

    protected long transitions;

    protected long lastUpdatedTransitions;

    protected int lastUpdatedStates;

    // ~ Constructors
    // ...........................................................

    public MyDefaultSearcher()
    {
    }

    // ~ Methods
    // ................................................................

    /**
     * @uml.property name="backtrackingInfos"
     */
    public ArrayList<ITransformationBacktrackingInfo> getBacktrackingInfos()
    {
        return backtrackingInfos;
    }

    public String getCopyrightNotice()
    {
        return null;
    }

    public int getErrorCount()
    {
        return errors;
    }

    public IMessageStore setOptions(String key, Properties configuration)
    {
        assert ((key != null) && (configuration != null));

        final String PRINT_COUNTER_EXAMPLES_ID = key
                                                 + "."
                                                 + MyDefaultSearcher.PRINT_COUNTER_EXAMPLES_ID;
        final String ALL_AS_ERRORS_ID = key + "."
                                        + MyDefaultSearcher.ALL_AS_ERRORS_ID;
        final String MAX_ERRORS_ID = key + "." + MyDefaultSearcher.MAX_ERRORS_ID;
        final String MAX_DEPTH_ID = key + "." + MyDefaultSearcher.MAX_DEPTH_ID;
        final String MAX_INVISIBLE_MOVES_ID = key
                                              + "."
                                              + MyDefaultSearcher.MAX_INVISIBLE_MOVES_ID;
        final String UPDATE_STATE_INCREMENT_ID = key
                                                 + "."
                                                 + MyDefaultSearcher.UPDATE_STATE_INCREMENT_ID;
        final String UPDATE_TRANSITION_INCREMENT_ID = key
                                                      + "."
                                                      + MyDefaultSearcher.UPDATE_TRANSITION_INCREMENT_ID;
        final String INVARIANTS_ID = key + "." + MyDefaultSearcher.INVARIANTS_ID;
        final String WRITE_TRAIL_FILE_ID = key
                                           + "."
                                           + MyDefaultSearcher.WRITE_TRAIL_FILE_ID;
        final String PRINT_VERBOSE_TRACE_ID = key
                                              + "."
                                              + MyDefaultSearcher.PRINT_VERBOSE_TRACE_ID;
        final String PRINT_STATUS_ID = key + "."
                                       + MyDefaultSearcher.PRINT_STATUS_ID;

        final String CHECK_BACKTRACK_ID = key + "."
                                          + MyDefaultSearcher.CHECK_BACKTRACK_ID;

        ArrayList<FileMessage> errors = new ArrayList<FileMessage>();
        ArrayList<FileMessage> warnings = new ArrayList<FileMessage>();

        for (Iterator<Object> i = configuration.keySet().iterator(); i
            .hasNext();)
        {
            String optionId = (String) i.next();
            String value = configuration.getProperty(optionId);

            if (PRINT_VERBOSE_TRACE_ID.equals(optionId))
            {
                try
                {
                    printVerboseTrace = Boolean.valueOf(value).booleanValue();
                }
                catch (Exception e)
                {
                    errors.add(FileMessage.buildMessage(
                        optionId,
                        ConfigurationMessages.BAD_FORMAT,
                        new String[]
                            {
                                optionId, "boolean", value
                            }));
                }
            }
            else if (WRITE_TRAIL_FILE_ID.equals(optionId))
            {
                try
                {
                    writeTrailFile = Boolean.valueOf(value).booleanValue();
                }
                catch (Exception e)
                {
                    errors.add(FileMessage.buildMessage(
                        optionId,
                        ConfigurationMessages.BAD_FORMAT,
                        new String[]
                            {
                                optionId, "boolean", value
                            }));
                }
            }
            else if (PRINT_STATUS_ID.equals(optionId))
            {
                try
                {
                    printStatus = Boolean.valueOf(value).booleanValue();
                }
                catch (Exception e)
                {
                    errors.add(FileMessage.buildMessage(
                        optionId,
                        ConfigurationMessages.BAD_FORMAT,
                        new String[]
                            {
                                optionId, "boolean", value
                            }));
                }
            }
            else if (PRINT_COUNTER_EXAMPLES_ID.equals(optionId))
            {
                try
                {
                    printCounterExamples = Boolean
                        .valueOf(value)
                        .booleanValue();
                }
                catch (Exception e)
                {
                    errors.add(FileMessage.buildMessage(
                        optionId,
                        ConfigurationMessages.BAD_FORMAT,
                        new String[]
                            {
                                optionId, "boolean", value
                            }));
                }
            }
            else if (ALL_AS_ERRORS_ID.equals(optionId))
            {
                try
                {
                    allAsErrors = Boolean.valueOf(value).booleanValue();
                }
                catch (Exception e)
                {
                    errors.add(FileMessage.buildMessage(
                        optionId,
                        ConfigurationMessages.BAD_FORMAT,
                        new String[]
                            {
                                optionId, "boolean", value
                            }));
                }
            }
            else if (CHECK_BACKTRACK_ID.equals(optionId))
            {
                try
                {
                    checkBacktrack = Boolean.valueOf(value).booleanValue();
                }
                catch (Exception e)
                {
                    errors.add(FileMessage.buildMessage(
                        optionId,
                        ConfigurationMessages.BAD_FORMAT,
                        new String[]
                            {
                                optionId, "boolean", value
                            }));
                }
            }
            else if (MAX_ERRORS_ID.equals(optionId))
            {
                try
                {
                    maxErrors = Integer.parseInt(value);
                }
                catch (Exception e)
                {
                    errors.add(FileMessage.buildMessage(
                        optionId,
                        ConfigurationMessages.BAD_FORMAT,
                        new String[]
                            {
                                optionId, "int", value
                            }));
                }
            }
            else if (MAX_DEPTH_ID.equals(optionId))
            {
                try
                {
                    maxDepth = Integer.parseInt(value);
                }
                catch (Exception e)
                {
                    errors.add(FileMessage.buildMessage(
                        optionId,
                        ConfigurationMessages.BAD_FORMAT,
                        new String[]
                            {
                                optionId, "int", value
                            }));
                }
            }
            else if (MAX_INVISIBLE_MOVES_ID.equals(optionId))
            {
                try
                {
                    maxInvisibleMoves = Integer.parseInt(value);
                }
                catch (Exception e)
                {
                    errors.add(FileMessage.buildMessage(
                        optionId,
                        ConfigurationMessages.BAD_FORMAT,
                        new String[]
                            {
                                optionId, "int", value
                            }));
                }
            }
            else if (UPDATE_STATE_INCREMENT_ID.equals(optionId))
            {
                try
                {
                    updateStateIncrement = Integer.parseInt(value);
                }
                catch (Exception e)
                {
                    errors.add(FileMessage.buildMessage(
                        optionId,
                        ConfigurationMessages.BAD_FORMAT,
                        new String[]
                            {
                                optionId, "int", value
                            }));
                }
            }
            else if (UPDATE_TRANSITION_INCREMENT_ID.equals(optionId))
            {
                try
                {
                    updateTransitionIncrement = Integer.parseInt(value);
                }
                catch (Exception e)
                {
                    errors.add(FileMessage.buildMessage(
                        optionId,
                        ConfigurationMessages.BAD_FORMAT,
                        new String[]
                            {
                                optionId, "int", value
                            }));
                }
            }
            else if (INVARIANTS_ID.equals(optionId))
            {
                try
                {
                    List<String> funIds = Util.splitCommaSeparatedList(value);
                    invariants = funIds.toArray(new String[funIds.size()]);
                }
                catch (Exception e)
                {
                    errors.add(FileMessage.buildMessage(
                        optionId,
                        ConfigurationMessages.BAD_FORMAT,
                        new String[]
                            {
                                optionId,
                                "comma-separated string list (no whitespace)",
                                "\"" + value + "\""
                            }));
                }
            }
            else if (optionId.startsWith(key) && !optionId.equals(key))
            {
                warnings.add(FileMessage.buildMessage(
                    optionId,
                    ConfigurationMessages.UNKNOWN_OPTION,
                    new String[]
                        {
                            optionId
                        }));
            }
        }

        return new DefaultMessageStore(errors, warnings);
    }

    /**
     * @uml.property name="state"
     */
    public IState getState()
    {
        return state;
    }

    /**
     * Once we have decided to terminate exploration of a depth-first path (the
     * precondition to this method), roll back changes until the first ancestor
     * state with unexplored siblings is found. If such an ancestor is found,
     * then execute one step on it and return <tt>true</tt>. If no explored
     * ancestor branches are found, then backtracking unwinds the entire trace
     * and the initial state is reached. A <tt>false</tt> return value signals
     * this result.
     */
    public boolean backtrack()
    {
        IState state = sr.getState();
        ArrayList<ITransformationBacktrackingInfo> stack = sr
            .getBacktrackingInfos();

        vf.backward();
        sf.backward();

        try
        {
            for (ListIterator<ITransformationBacktrackingInfo> tbiIter = stack
                .listIterator(stack.size()); tbiIter.hasPrevious();)
            {
                // Peek at the transformation
                ITransformationBacktrackingInfo tbi = tbiIter.previous();

                int threadId = tbi.getTransition().first;
                Transformation transformation = tbi.getTransition().second;

                vf.setContext(state, threadId);
                sf.setContext(state, threadId);

                currentDepth--;
                sf.getNotifier().notifyCurrentDepthChanged(
                    currentDepth + 1,
                    currentDepth);

                ArrayList<IPostNextStateBacktrackingInfo> postNextStateInfos = tbi
                    .getPostNextStateBacktrackingInfos();
                ArrayList<INextStateBacktrackingInfo> nextStateInfos = tbi
                    .getNextStateBacktrackingInfos();
                ArrayList< ? extends IActionBacktrackingInfo> mainInfos = tbi
                    .getMainTransformationBacktrackingInfos();

                // Roll back search metadata actions (property automaton
                // transitions, state coalescing data, etc)
                for (ListIterator<IPostNextStateBacktrackingInfo> pnsIter = postNextStateInfos
                    .listIterator(postNextStateInfos.size()); pnsIter
                    .hasPrevious();)
                {
                    IPostNextStateBacktrackingInfo bi = pnsIter.previous();
                    pnsIter.remove();

                    bi.backtrack(state);

                    // If nondeterminism still needs to be explored, then quit
                    // rolling change back, restart from here, and exit
                    if (!bi.getSchedulingStrategyInfo().isCovered())
                    {
                        isInvisible = false;
                        stateId = tbi.getStateId();
                        seenState = false;

                        vf.forward();
                        sf.forward();

                        doPostNextStateBookkeeping(tbi, bi);

                        currentDepth++;
                        sf.getNotifier().notifyCurrentDepthChanged(
                            currentDepth - 1,
                            currentDepth);

                        if (sr.shouldStore())
                        {
                            IStoreStateResult newState = sm.storeState(state);
                            stateId = newState.getStateId();
                            seenState = newState.isSeen();
                        }

                        return true;
                    }
                }

                // Roll back actions to set up next-state
                for (ListIterator<INextStateBacktrackingInfo> nsIter = nextStateInfos
                    .listIterator(nextStateInfos.size()); nsIter.hasPrevious();)
                {
                    nsIter.previous().backtrack(state);
                    nsIter.remove();
                }

                // Roll back main transformation body actions
                for (ListIterator< ? extends IActionBacktrackingInfo> mainIter = mainInfos
                    .listIterator(mainInfos.size()); mainIter.hasPrevious();)
                {
                    IActionBacktrackingInfo bi = mainIter.previous();
                    mainIter.remove();

                    bi.backtrack(state);

                    if (!bi.getSchedulingStrategyInfo().isCovered())
                    {
                        isInvisible = false;
                        stateId = tbi.getStateId();
                        seenState = false;

                        vf.forward();
                        sf.forward();

                        this.invisibleMoves = tbi.getInvisibleMoves();

                        vf.setContext(state, threadId);
                        sf.setContext(state, threadId);

                        sr.doTransition(threadId, transformation, tbi
                            .getAppropriateRestartPoint(bi), tbi);

                        return true;

                    }
                }

                //
                // All sub-parts of the transition have been rolled back
                // by now. Only nondeterminism on the selection of the overall
                // transition remains.
                //

                this.seenState = false;
                this.invisibleMoves = tbi.getInvisibleMoves();
                this.stateId = tbi.getStateId();
                this.lastMovedThreadId = tbi.getLastMovedThreadId();

                // Pop the transformation
                tbiIter.remove();
                tbi.backtrack(state);

                if (checkBacktrack)
                {
                    assert sm.storeState(state).getStateId() == tbi
                        .getStateId();
                }

                if (!tbi.getSchedulingStrategyInfo().isCovered())
                {
                    ArrayList<Pair<Integer, Transformation>> workSet = tbi
                        .getWorkSet();
                    ArrayList<Pair<Integer, Transformation>> enabledSet = tbi
                        .getEnabledSet();

                    ISchedulingStrategyInfo ssi = tbi
                        .getSchedulingStrategyInfo();

                    int workSetIndex = ss.advise(createContext(
                        stateId,
                        invisibleMoves,
                        0,
                        state), workSet, ssi);

                    Pair<Integer, Transformation> restartTransformation = workSet
                        .get(workSetIndex);

                    int[] tids = state.getThreadIds();
                    Arrays.sort(tids);

                    int canonicalThreadIndex = Util.search(
                        tids,
                        restartTransformation.first);

                    ITransformationBacktrackingInfo newTbi;

                    if (restartTransformation.second instanceof BlockTransformation)
                    {
                        newTbi = bif.createBlockTransformationBacktrackingInfo(
                            stateId,
                            invisibleMoves,
                            isInvisible,
                            lastMovedThreadId,
                            enabledSet,
                            workSet,
                            workSet.get(workSetIndex),
                            canonicalThreadIndex,
                            ssi);
                    }
                    else
                    {
                        assert restartTransformation.second instanceof InvokeTransformation;

                        newTbi = bif
                            .createInvokeTransformationBacktrackingInfo(
                                stateId,
                                invisibleMoves,
                                isInvisible,
                                lastMovedThreadId,
                                enabledSet,
                                workSet,
                                workSet.get(workSetIndex),
                                canonicalThreadIndex,
                                ssi);
                    }

                    sr.getBacktrackingInfos().add(newTbi);

                    lastMovedThreadId = restartTransformation.first;

                    vf.forward();
                    sf.forward();
                    vf.setContext(state, restartTransformation.first);
                    sf.setContext(state, restartTransformation.first);

                    sr.doTransition(
                        restartTransformation.first,
                        restartTransformation.second,
                        null,
                        newTbi);
                    vf.removeContext();
                    sf.removeContext();

                    return true;
                }
            }

            // Okay... no transitions needing more exploration were found.
            // A null return value signifies the no restart is necessary.
            return false;
        }
        finally
        {
            vf.removeContext();
            sf.removeContext();

            vf.forward();
            sf.forward();
        }
    }

    public IMessageStore connect(IBogorConfiguration bc)
    {
        assert (bc != null);

        ArrayList<FileMessage> errors = new ArrayList<FileMessage>();
        ArrayList<FileMessage> warnings = new ArrayList<FileMessage>();

        this.bc = bc;
        this.sr = bc.getSearcher();
        this.symbolTable = bc.getSymbolTable();
        this.at = bc.getActionTaker();
        this.cew = bc.getCounterExampleWriter();
        this.sm = bc.getStateManager();
        this.ss = bc.getSchedulingStrategist();
        this.tr = bc.getTransformer();
        this.ee = bc.getExpEvaluator();
        this.sf = bc.getStateFactory();
        this.vf = bc.getValueFactory();
        this.bif = bc.getBacktrackingInfoFactory();
        this.pm = bc.getProgressManager();
        this.pw = bc.getPrintWriter();

        // TODO: needs to check for invariants type
        if (invariants != null)
        {
            ArrayList<String> list = new ArrayList<String>();
            int size = invariants.length;
            Map<String, Type> funMap = symbolTable.getGlobalFunTable();

            for (int i = 0; i < size; i++)
            {
                String funId = invariants[i];
                Type type = funMap.get(funId);

                if (!(type instanceof FunType))
                {
                    errors.add(FileMessage.buildMessage(
                        "No such invariant fun {0}.",
                        new String[]
                            {
                                funId
                            }));

                    continue;
                }

                FunType fType = (FunType) type;

                if ((fType.getParamTypeCount() != 0)
                    || !(fType.getReturnType() instanceof BooleanType))
                {
                    errors.add(FileMessage.buildMessage(
                        "Ill-formed invariant {0} of type {1}",
                        new String[]
                            {
                                funId, fType.toString()
                            }));

                    continue;
                }

                list.add(funId);
            }

            size = list.size();

            if (size == 0)
            {
                invariants = null;
            }
            else
            {
                invariants = new String[size];

                for (int i = 0; i < size; i++)
                {
                    invariants[i] = (String) list.get(i);
                }
            }
        }

        return new DefaultMessageStore(errors, warnings);
    }

    public IState createInitialState()
    {
        IStateFactoryArguments args = getInitialStateFactoryArguments();
        IState vanillaState = sf.createState(args);
        fillInitialVariableValues(vanillaState, args);
        return vanillaState;
    }

    public void dispose()
    {
        bc = null;
        symbolTable = null;
        at = null;
        sm = null;
        ss = null;
        tr = null;
        ee = null;
        sf = null;
        vf = null;
        bif = null;
        pm = null;
        pw = null;
        sr = null;

        if (cew != null)
        {
            cew.dispose();
            cew = null;
        }
    }

    public void doTransition(
        int threadId,
        Transformation t,
        Action a,
        ITransformationBacktrackingInfo container)
    {
    	
        assert (t != null);

        ISchedulingStrategyContext ssc = createContext(
            stateId,
            invisibleMoves,
            threadId,
            state);

        isInvisible = t.getVisibility() == Visibility.INVISIBLE;

        doTransition(ssc, t, a, isInvisible, container);
        doPostNextStateBookkeeping(container, null);

        IExceptionBacktrackingInfo raisedException = Util.findLast(container
            .getNextStateBacktrackingInfos(), IExceptionBacktrackingInfo.class);

        if ((raisedException != null && raisedException.isUncaught())
            || !state.isThreadAlive(threadId)
            || invisibleMoves >= maxInvisibleMoves)
        {
            isInvisible = false;
        }

        sr.store();
        
        if(sr.shouldStore()){
        	System.out.println(container.getStateId());
        	System.out.println(container.getTransition());
        }

        transitions++;
        currentDepth++;
        sf.getNotifier().notifyCurrentDepthChanged(
            currentDepth - 1,
            currentDepth);

        if (currentDepth > currentMaxDepth)
        {
            currentMaxDepth = currentDepth;
        }

        if (printStatus)
        {
            int numStates = sm.getStateCount();
            int totalStates = numStates + seenStates;

            if ((lastUpdatedStates <= totalStates)
                || (lastUpdatedTransitions <= transitions))
            {
                lastUpdatedStates += updateStateIncrement;
                lastUpdatedTransitions += updateTransitionIncrement;
                pm.update(
                    transitions,
                    numStates,
                    seenStates,
                    currentDepth,
                    currentMaxDepth,
                    errors,
                    System.currentTimeMillis() - startTime,
                    false);
            }
        }
    }

    public void error(int errCode)
    {
        // be sure that error state is always in state manager
        sm.storeState(state);

        errors++;

        pw.println();

        if (printCounterExamples)
        {
            pw.println("*** Begin Error Trace ***");

            for (Iterator<ITransformationBacktrackingInfo> iter = sr
                .getBacktrackingInfos()
                .iterator(); iter.hasNext();)
            {
                ITransformationBacktrackingInfo transition = iter.next();

                int thread = transition.getTransition().first;
                Transformation transformation = transition.getTransition().second;

                pw.printf(
                    "Thread#%d, Line#%d, FSM:%s, Loc:%s",
                    thread,
                    transformation.getLocationInfo().getLine1(),
                    transformation.getParent().getParent().getId(),
                    transformation.getParent().getId());

                pw.println();
                pw.println(transformation);
                pw.println();
            }

            pw.println("*** End Error Trace ***");
        }

        pw.print("[Time: ");
        pw.print(System.currentTimeMillis() - startTime);
        pw.print(" ms, Depth: ");
        pw.print(currentDepth);
        pw.print("] Error found: ");

        String reason = null;

        // Do this once, rather than duplicating the code
        // for each upcoming "case" branch...
        pm.update(
            transitions,
            sm.getStateCount(),
            seenStates,
            currentDepth,
            currentMaxDepth,
            errors,
            System.currentTimeMillis() - startTime,
            false);

        switch (errCode)
        {
            case ILL_FORMED_MODEL_CODE:
                pm.signalIllFormedModel();
                pw.println(reason = "Ill-formed model");

                break;

            case INVALID_END_STATE_CODE:
                pm.signalInvalidEndState();
                pw.println(reason = "Invalid end state");

                break;

            case ASSERTION_FAILED_CODE:
                pm.signalAssertionFailure();
                pw.println(reason = "Assertion failed");

                break;

            case RANGE_EXCEPTION_CODE:
                pm.signalRangeException();
                pw.println(reason = "Range exception");

                break;

            case UNCAUGHT_EXCEPTION_CODE:
                pm.signalUncaughtException();
                pw.print(reason = "Uncaught exception: ");

                ITransformationBacktrackingInfo tbi = sr
                    .getBacktrackingInfos()
                    .get(sr.getBacktrackingInfos().size() - 1);
                IExceptionBacktrackingInfo xbi = Util.findLast(
                    tbi.getNextStateBacktrackingInfos(),
                    IExceptionBacktrackingInfo.class);

                if (xbi != null)
                {
                    assert xbi.isUncaught();
                    BogorException be = xbi.getThrownException();

                    if (be instanceof ArithmeticBogorException)
                    {
                        pw.println("arithmetic (e.g., divide by zero)");
                    }
                    else if (be instanceof BadMonitorBogorException)
                    {
                        pw.println("cad monitor");
                    }
                    else if (be instanceof CastBogorException)
                    {
                        pw.println("cast");
                    }
                    else if (be instanceof IndexOutOfBoundsBogorException)
                    {
                        pw.println("index out of bounds");
                    }
                    else if (be instanceof NullPointerBogorException)
                    {
                        pw.println("null pointer");
                    }
                    else if (be instanceof ExceptionThrownBogorException)
                    {
                        ExceptionThrownBogorException etbe = (ExceptionThrownBogorException) be;
                        pw.println(etbe.getThrowableName());
                    }
                }
                break;

            case EXT_FAILED_CODE:
                pm.signalExtFailure();
                pw.println(reason = "Ext failed");

                break;

            case INVARIANT_VIOLATED_CODE:
                pm.signalInvariantViolation();
                pw.println(reason = "Invariant violated");

                break;

            default:
                assert false;

                break;
        }

        if (!allAsErrors)
        {
            storeCounterExample(
                sr.getBacktrackingInfos(),
                stateId,
                invisibleMoves,
                reason);
        }

        pw.println();

        if (errors == maxErrors)
        {
            throw new MaxErrorReachedException();
        }
    }

    public void initialize()
    {
        backtrackingInfos = new ArrayList<ITransformationBacktrackingInfo>();
        isInvisible = false;
        lastMovedThreadId = -1;
        invisibleMoves = 0;
        transitions = 0;
        lastUpdatedStates = 0;
        lastUpdatedTransitions = 0;
        errors = 0;
        seenStates = 0;
        currentDepth = 0;

        state = sr.createInitialState();
        stateId = sm.storeState(state).getStateId();

        vf.forward();
        sf.forward();
    }

    public void search()
    {
        System.gc();

        pw.println("");

        String startMemoryMsg = "Total memory before search: "
                                + getMemory(Runtime.getRuntime().totalMemory()
                                            - Runtime.getRuntime().freeMemory());

        boolean maxDepthReached = false;

        startTime = System.currentTimeMillis();

        try
        {
            while (!pm.shouldTerminate())
            {
                if (currentDepth > maxDepth)
                {
                    if (allAsErrors)
                    {
                        // TODO: change to call to error()
                        errors++;
                        storeCounterExample(
                            sr.getBacktrackingInfos(),
                            stateId,
                            invisibleMoves,
                            "Max Depth Reached");

                        if (errors == maxErrors)
                        {
                            throw new MaxErrorReachedException();
                        }
                    }

                    currentMaxDepth--;
                    maxDepthReached = true;
                    pm.signalMaxDepthReached();

                    if (!sr.backtrack())
                    {
                        // finish
                        break;
                    }
                }
                else if (!sr.step())
                {
                    if (allAsErrors)
                    {
                        // TODO: change to call to error()
                        errors++;
                        storeCounterExample(
                            sr.getBacktrackingInfos(),
                            stateId,
                            invisibleMoves,
                            "Seen Before or End State");

                        if (errors == maxErrors)
                        {
                            throw new MaxErrorReachedException();
                        }
                    }

                    if (!sr.backtrack())
                    {
                        // finish
                        break;
                    }
                }

                // handle uncaught BIR-level exceptions
                checkExceptions();

                if (!checkInvariants())
                {
                    sr.error(INVARIANT_VIOLATED_CODE);

                    if (!sr.backtrack())
                    {
                        // finish
                        break;
                    }
                }
            }
        }
        catch (MaxErrorReachedException mce)
        {
        }
        catch (OutOfMemoryError oeme)
        {
            pm.signalOutOfMemory();
            pw.println("Out of memory!!!");
        }

        long endTime = System.currentTimeMillis();

        System.gc();

        pm.update(
            transitions,
            sm.getStateCount(),
            seenStates,
            currentDepth,
            currentMaxDepth,
            errors,
            endTime - startTime,
            true);

        if (maxDepthReached)
        {
            pw.println("");
            pw.println("Max depth reached!!!");
            pw.println("");
        }

        System.gc();

        int states = sm.getStateCount();
        long processingTime = endTime - startTime;

        System.gc();

        pw.println(startMemoryMsg);
        pw.println("Total memory after search: "
                   + getMemory(Runtime.getRuntime().totalMemory()
                               - Runtime.getRuntime().freeMemory()));
        pw.println("Total search time: " + processingTime + " ms ("
                   + getTime(processingTime) + ")");
        pw.println("States count: " + states);
        pw.println("Matched states count: " + seenStates);
        pw.println("Max depth: " + currentMaxDepth);
        pw.flush();

        sr.writeCounterExamples();

        pw.println("Done!");
        pw.flush();

        return;
    }

    public boolean shouldStore()
    {
        return checkBacktrack || !isInvisible;
    }

    public boolean step()
    {
        if (shouldBacktrack() || seenState)
        {
            return false;
        }

        final int[] runnableThreadIds = state.getThreadIds();

        if (runnableThreadIds.length == 0)
        {
            return false;
        }

        IntObjectTable<ArrayList<Transformation>> workSet;
        IntObjectTable<ArrayList<Transformation>> enabledSet;

        try
        {
            if (isInvisible)
            {
                IEnabledTransformationsContext ctx = createContext(
                    state,
                    stateId,
                    invisibleMoves,
                    new int[]
                        {
                            lastMovedThreadId
                        });

                enabledSet = ss.getEnabledTransformations(ctx);
                workSet = ss.getWorkSet(ctx, enabledSet);

                if (workSet.size() == 0)
                {
                    isInvisible = false;

                    if (!sr.store())
                    {
                        return false;
                    }

                    ctx = createContext(
                        state,
                        stateId,
                        invisibleMoves,
                        runnableThreadIds);

                    enabledSet = ss.getEnabledTransformations(ctx);
                    workSet = ss.getWorkSet(ctx, enabledSet);
                }
            }
            else
            {
                IEnabledTransformationsContext ctx = createContext(
                    state,
                    stateId,
                    invisibleMoves,
                    runnableThreadIds);

                enabledSet = ss.getEnabledTransformations(ctx);
                workSet = ss.getWorkSet(ctx, enabledSet);
            }
        }
        catch (IllFormedModelBogorException ifmmce)
        {
            sr.error(ILL_FORMED_MODEL_CODE);

            pw.println(ifmmce.getNode());
            pw.println();

            return false;
        }

        int workSetSize = 0;

        for (int key : workSet.keys())
        {
            workSetSize += workSet.get(key).size();
        }

        if (workSetSize == 0)
        {
            sr.error(INVALID_END_STATE_CODE);
            return false;
        }

        int enabledSetSize = 0;

        for (int key : enabledSet.keys())
        {
            enabledSetSize += enabledSet.get(key).size();
        }

        ISchedulingStrategyInfo ssi = ss.newStrategyInfo();

        ArrayList<Pair<Integer, Transformation>> flattenedWorkSet = makeChoices(workSet);

        ArrayList<Pair<Integer, Transformation>> flattenedEnabledSet = makeChoices(enabledSet);

        // Ask scheduler which entry from workset to use
        Pair<Integer, Transformation> workSetEntry = flattenedWorkSet.get(ss
            .advise(
                createContext(stateId, invisibleMoves, 0, state),
                flattenedWorkSet,
                ssi));

        int[] tids = state.getThreadIds();
        Arrays.sort(tids);

        int canonicalThreadIndex = Util.search(tids, workSetEntry.first);

        ITransformationBacktrackingInfo container;

        if (workSetEntry.second instanceof BlockTransformation)
        {
            container = bif.createBlockTransformationBacktrackingInfo(
                stateId,
                invisibleMoves,
                isInvisible,
                lastMovedThreadId,
                flattenedEnabledSet,
                flattenedWorkSet,
                workSetEntry,
                canonicalThreadIndex,
                ssi);
        }
        else
        {
            container = bif.createInvokeTransformationBacktrackingInfo(
                stateId,
                invisibleMoves,
                isInvisible,
                lastMovedThreadId,
                flattenedEnabledSet,
                flattenedWorkSet,
                workSetEntry,
                canonicalThreadIndex,
                ssi);
        }

        sr.getBacktrackingInfos().add(container);

        lastMovedThreadId = workSetEntry.first;

        vf.setContext(state, workSetEntry.first);
        sf.setContext(state, workSetEntry.first);

        sr.doTransition(
            workSetEntry.first,
            workSetEntry.second,
            null,
            container);

        sf.removeContext();

        return true;
    }

    /**
     * Rolls back the state to the moment just before the most recent
     * transition.
     * 
     * @param state
     *            system state to revert
     * @param backtrackingInfos
     *            stack of reverse deltas to roll back state
     * @return the <code>ITransformationsBacktrackingInfo</code> of the most
     *         recent transition (incomplete)
     */

    public boolean stepBackward()
    {
        ArrayList<ITransformationBacktrackingInfo> stack = sr
            .getBacktrackingInfos();
        IState state = sr.getState();

        if (stack.isEmpty())
        {
            return false;
        }

        // Pop last transition off stack
        ITransformationBacktrackingInfo tbi = stack.remove(stack.size() - 1);

        vf.backward();
        sf.backward();

        int threadId = tbi.getTransition().first;

        vf.setContext(state, threadId);
        sf.setContext(state, threadId);

        currentDepth--;
        sf.getNotifier().notifyCurrentDepthChanged(
            currentDepth + 1,
            currentDepth);

        ArrayList<IPostNextStateBacktrackingInfo> postNextStateInfos = tbi
            .getPostNextStateBacktrackingInfos();
        ArrayList<INextStateBacktrackingInfo> nextStateInfos = tbi
            .getNextStateBacktrackingInfos();
        ArrayList< ? extends IActionBacktrackingInfo> mainInfos = tbi
            .getMainTransformationBacktrackingInfos();

        // Roll back search metadata actions (property automaton
        // transitions,
        // state coalescing data, etc)
        for (ListIterator<IPostNextStateBacktrackingInfo> pnsIter = postNextStateInfos
            .listIterator(postNextStateInfos.size()); pnsIter.hasPrevious();)
        {
            IPostNextStateBacktrackingInfo bi = pnsIter.previous();
            pnsIter.remove();

            bi.backtrack(state);
        }

        // Roll back actions to set up next-state
        for (ListIterator<INextStateBacktrackingInfo> nsIter = nextStateInfos
            .listIterator(nextStateInfos.size()); nsIter.hasPrevious();)
        {
            nsIter.previous().backtrack(state);
            nsIter.remove();
        }

        // Roll back main transformation body actions
        for (ListIterator< ? extends IActionBacktrackingInfo> mainIter = mainInfos
            .listIterator(mainInfos.size()); mainIter.hasPrevious();)
        {
            IActionBacktrackingInfo bi = mainIter.previous();
            mainIter.remove();

            bi.backtrack(state);
        }

        //
        // All sub-parts of the transition have been rolled back
        // by now. Only nondeterminism on the selection of which
        // transition remains.
        //

        this.invisibleMoves = tbi.getInvisibleMoves();
        this.stateId = tbi.getStateId();
        this.lastMovedThreadId = tbi.getLastMovedThreadId();

        isInvisible = false;
        stateId = tbi.getStateId();
        seenState = false;

        tbi.backtrack(state);

        vf.removeContext();
        sf.removeContext();

        vf.forward();
        sf.forward();

        return true;
    }

    public boolean store()
    {
        if (sr.shouldStore())
        {
            IStoreStateResult result = sm.storeState(state);
            stateId = result.getStateId();
            seenState = result.isSeen();
            invisibleMoves = 0;

            if (seenState)
            {
                seenStates++;

                return false;
            }
        }
        else
        {
            invisibleMoves++;
        }

        return true;
    }

    public void writeCounterExamples()
    {
        if (writeTrailFile)
        {
            cew.writeCounterExamples();
        }
    }

    protected FSMSymbolTable getFSMSymbolTable(int locDesc)
    {
        return symbolTable.getFSMSymbolTable(locDesc);
    }

    protected FSMSymbolTable getFSMSymbolTable(IState state, int threadId)
    {
        int locDesc = state.getLocation(threadId);

        return getFSMSymbolTable(locDesc);
    }

    protected IStateFactoryArguments getInitialStateFactoryArguments()
    {
        // construct reverse (index --> name) globals identifier mapping
        IntObjectTable<String> globalNameMap = new IntObjectTable<String>();

        {
            for (String key : symbolTable.getGlobalIndexTable().keySet(true))
            {
                globalNameMap.put(
                    symbolTable.getGlobalIndexTable().get(key),
                    key);
            }
        }

        ArrayList<Type> globalTypes = symbolTable.getGlobalTypes();
        int globalsCount = globalTypes.size();
        IValue[] globalValues = new IValue[globalsCount];

        for (int i = 0; i < globalsCount; i++)
        {
            String name = globalNameMap.get(i);
            Global astNode = (Global) symbolTable.getIdentifierDefTable().get(
                name);
            Type globalType = globalTypes.get(i);

            // For now, we just create the default value. A global
            // whose initial value was specified in the model will
            // be initialized immediately after the IState is instantiated.
            globalValues[i] = vf.createDefaultValue(globalType);
        }

        final IValueArray globalValueArray = vf
            .newVariedValueArray(globalValues);

        final IntObjectTable<IValueArray> threadLocalValuesTable = new IntObjectTable<IValueArray>();
        final IntIntTable threadLocationTable = new IntIntTable();

        // loop over each thread type defined to instantiate any active ones
        for (FSMSymbolTable fsmSymbolTable : symbolTable
            .getFunctionTable()
            .values())
        {
            FSM fsm = fsmSymbolTable.getFSM();

            // if the isn't an active type, then no default instance is
            // created
            if (!shouldActivateThread(fsm))
            {
                continue;
            }

            int numCopies = fsm.getOptionalActiveMultiplicityExp() != null
                ? new ConstIntExpEvaluator(symbolTable).getValue(
                    fsm.getOptionalActiveMultiplicityExp()).intValue()
                : 1;

            for (int j = 0; j < numCopies; j++)
            {
                ArrayList<Type> localTypes = fsmSymbolTable.getLocalTypes();
                int localsCount = localTypes.size();
                int argsCount = fsm.getParamCount();

                // All active thread types have exactly zero or one
                // parameters.
                assert (argsCount == 0) || (argsCount == 1);

                IValue[] localValues = new IValue[localsCount + argsCount];

                for (int k = 0; k < argsCount; k++)
                {
                    // The single allowed parameter to an active thread
                    // type is an integer giving its index in the
                    // replicated thread array.
                    // Type-checker should enforce that type of
                    // this parameter is integer.
                    localValues[k] = vf.newIntValue(j);
                }

                for (int k = 0; k < localsCount; k++)
                {
                    Local astLocal = fsm.getLocal(k);
                    Type localType = localTypes.get(k);

                    // Just give the local the default values for now. If an
                    // initial value was specified, it will be filled in
                    // immediately after the IState is instantiated.
                    localValues[k + argsCount] = vf
                        .createDefaultValue(localType);
                }

                IValueArray localValueArray = vf
                    .newVariedValueArray(localValues);

                int tid = sf.newThreadDescriptor();

                String locId = fsmSymbolTable.getInitialLocation();
                final int locDesc = fsmSymbolTable.getLocationDescTable().get(
                    locId);

                threadLocalValuesTable.put(tid, localValueArray);
                threadLocationTable.put(tid, locDesc);
            }
        }

        return new IStateFactoryArguments()
            {
                public IValueArray getGlobalValues()
                {
                    return globalValueArray;
                }

                public IValueArray getLocalValues(int threadId)
                {
                    assert threadLocalValuesTable.containsKey(threadId);

                    return threadLocalValuesTable.get(threadId);
                }

                public int getLocationDesc(int threadId)
                {
                    assert threadLocalValuesTable.containsKey(threadId);

                    return threadLocationTable.get(threadId);
                }

                public int[] getThreadIds()
                {
                    return threadLocationTable.keys();
                }
            };
    }

    protected Location getLocation(IState state, int threadId)
    {
        int locDesc = state.getLocation(threadId);

        return getLocation(locDesc);
    }

    protected Location getLocation(int locDesc)
    {
        String locId = symbolTable.getLocDescLocIdTable()[locDesc];
        Location l = getFSMSymbolTable(locDesc)
            .getLocationDefTable()
            .get(locId);

        return l;
    }

    protected String getMemory(long mem)
    {
        return new DecimalFormat("#,###").format(mem) + " bytes ("
               + new DecimalFormat("#,###.##").format(mem / 1024.0 / 1024.0)
               + " Mb)";
    }

    protected String getTime(long time)
    {
        int hours = (int) (time / 3600000);
        time = time - (hours * 3600000L);

        int minutes = (int) (time / 60000);
        time = time - (minutes * 60000L);

        int seconds = (int) (time / 1000);

        return hours + ":" + minutes + ":" + seconds;
    }

    protected void addAll(
        ArrayList<IBacktrackingInfo> result,
        IBacktrackingInfo[] bis)
    {
        int size = bis.length;

        for (int i = 0; i < size; i++)
        {
            result.add(bis[i]);
        }
    }

    protected void checkExceptions()
    {
        ArrayList<ITransformationBacktrackingInfo> stack = sr
            .getBacktrackingInfos();

        if (!stack.isEmpty())
        {
            ITransformationBacktrackingInfo lastTbi = stack
                .get(stack.size() - 1);

            IExceptionBacktrackingInfo xbi = Util.findLast(
                lastTbi.getNextStateBacktrackingInfos(),
                IExceptionBacktrackingInfo.class);

            if (xbi != null && xbi.isUncaught())
            {
                BogorException mce = xbi.getThrownException();

                if (mce instanceof AssertionBogorException)
                {
                    sr.error(ASSERTION_FAILED_CODE);
                }
                else if (mce instanceof RangeBogorException)
                {
                    sr.error(RANGE_EXCEPTION_CODE);
                }
                else if (mce instanceof ExtFailedBogorException)
                {
                    sr.error(EXT_FAILED_CODE);
                }
                else if (mce instanceof ExceptionThrownBogorException)
                {
                    sr.error(UNCAUGHT_EXCEPTION_CODE);
                }
            }
        }
    }

    protected boolean checkInvariants()
    {
        if (invariants == null)
        {
            return true;
        }

        int size = invariants.length;
        boolean result = true;

        for (int i = 0; (i < size) && result; i++)
        {
            String funId = invariants[i];
            ISchedulingStrategyInfo ssi = ss.newStrategyInfo();
            ISchedulingStrategyContext ssc = createContext(-1, -1, -1, state);

            ee.setSchedulingStrategyContextInfo(ssc, ssi);

            do
            {
                IValue val = ee.evaluateApply(funId, new IValue[0]);
                assert val instanceof IIntValue;

                if (((IIntValue) val).getInteger() == 0)
                {
                    result = false;
                }
            }
            while (!ssi.isCovered());

            ee.unsetSchedulingStrategyContextInfo();
        }

        return result;
    }

    protected ISchedulingStrategyContext createContext(
        final int stateId,
        final int invisibleMoves,
        final int threadId,
        final IState state)
    {
        return new ISchedulingStrategyContext()
            {
                public void dispose()
                {
                }

                public int getExtDesc()
                {
                    return 0;
                }

                public IState getState()
                {
                    return state;
                }

                public int getInvisibleMoves()
                {
                    return invisibleMoves;
                }

                public int getThreadId()
                {
                    return threadId;
                }

                public int getStateId()
                {
                    return stateId;
                }
            };
    }

    protected IEnabledTransformationsContext createContext(
        final IState state,
        final int stateId,
        final int invisibleMoves,
        final int[] threadIds)
    {
        return new IEnabledTransformationsContext()
            {
                public IState getState()
                {
                    return state;
                }

                public int getStateId()
                {
                    return stateId;
                }

                public int getInvisibleMoves()
                {
                    return invisibleMoves;
                }

                public int[] getThreadIds()
                {
                    return threadIds;
                }
            };
    }

    /**
     * <p>
     * Perform any steps needed to update the machinery after the main
     * transition has been executed. Property automaton moves, updates to
     * fields, etc. <em>Every</em> action performed inside the scope of this
     * method should be reversible via an <tt>IBacktrackingInfo</tt>. The
     * reverse actions should be added to the end of <tt>container</tt>'s
     * {@link ITransformationBacktrackingInfo#getPostNextStateBacktrackingInfos()
     * post-next state undo actions} collection.
     * </p>
     * <p>
     * Note that the parameter <tt>restartPoint</tt> may indicate a point from
     * which the machinery updates should begin. This is used in the case that
     * backtracking detects one of the actions inserted onto the stack from a
     * prior invocation of <tt>doPostNextStateBookkeeping()</tt> needs further
     * exploration. In this case, the exact backtracking record put on the stack
     * last time is passed in as a reference item. Its scheduling information (<tt>restartPoint.getSchedulingStrategyInfo()</tt>)
     * should be used to help determine the next branch to explore.
     * </p>
     * <p>
     * In the case that <tt>restartPoint</tt> is specified (not <tt>null</tt>),
     * an implementor is obliged to check whether its runtime type corresponds
     * to any action which they (not the base class) have put onto the stack. If
     * so, then no recursive call to <tt>super.doPostNextStateBookkeeping()</tt>
     * is made. If <tt>restartPoint</tt> is not <tt>null</tt> but its
     * runtime type does not match any item explicitly put onto the stack by the
     * implementor, then the superclass's implementation should be invoked in
     * order to allow <em>its</em> implementor the opportunity to handle the
     * not-yet-fully-explored branch point. An example:
     * </p>
     * 
     * <pre>
     *  protected void doPostNextStateBookkeeping(
     *      ITransformationBacktrackingInfo container,
     *      IPostNextStateBacktrackingInfo restartPoint)
     *  {
     *      if (restartPoint instanceof IPrivateFieldUpdateBacktrackingInfo)
     *      {
     *          updatePrivateField(
     *              container,
     *              (IPrivateFieldUpdateBacktrackingInfo) restartPoint);
     *      }
     *      else
     *      {
     *          super.doPostNextStateBookkeeping(container, restartPoint);
     *          updatePrivateField(container, null);
     *      }
     *  }
     *  
     *  protected void updatePrivateField(
     *      IPostNextStateBacktrackingInfo container,
     *      IPrivateFieldUpdateBacktrackingInfo restartPoint)
     *  {
     *      final ISchedulingStrategyInfo ssi = restartPoint == null
     *          ? ss.newStrategyInfo()
     *          : restartPoint.getSchedulingStrategyInfo();
     *           
     *      final int oldValue = this.someFunkyVariable;
     *      
     *      int newValue = ... ;
     *      
     *      this.someFunkyVariable = newValue;
     *      
     *      container.getPostNextStateBacktrackingInfos().add(
     *          new IPrivateFieldUpdateBacktrackingInfo()
     *              {
     *                  ...
     *                  
     *                  public void backtrack(IState state)
     *                  {
     *                      someFunkyVariable = oldValue;
     *                  }
     *                  
     *                  public ISchedulingStrategyInfo getSchedulingStrategyInfo()
     *                  {
     *                      return ssi;
     *                  }
     *                  
     *                  ...
     *              });
     *  }
     * </pre>
     */
    protected void doPostNextStateBookkeeping(
        ITransformationBacktrackingInfo container,
        IPostNextStateBacktrackingInfo restartPoint)
    {
        // do nothing in default version
    }

    protected void doTransition(
        ISchedulingStrategyContext ssc,
        Transformation t,
        Action a,
        boolean isInvisible,
        ITransformationBacktrackingInfo container)
    {	
        if (t instanceof BlockTransformation)
        {
            BlockTransformation bt = (BlockTransformation) t;
            tr.transform(ssc, bt, isInvisible, a, container);
        }
        else if (t instanceof InvokeTransformation)
        {	
            InvokeTransformation it = (InvokeTransformation) t;
            tr.transform(ssc, it, isInvisible, false, null, container);
        }
        else
        {
            assert false;
        }
    }

    protected ArrayList<ICounterExampleSchedulingInfo> extractErrorSchedule(
        ArrayList<ITransformationBacktrackingInfo> stack)
    {
        ArrayList<ICounterExampleSchedulingInfo> result = new ArrayList<ICounterExampleSchedulingInfo>();

        for (Iterator<ITransformationBacktrackingInfo> transitions = stack
            .iterator(); transitions.hasNext();)
        {
            IntList currNumOfChoices = new IntList();
            IntList currChosenIndices = new IntList();

            ITransformationBacktrackingInfo tbi = transitions.next();
            Pair<Integer, Transformation> transition = tbi.getTransition();

            // find index of transition.second in containing Location
            int transformationIndex = 0;
            while (transition.second != transition.second
                .getParent()
                .getTransformation(transformationIndex))
            {
                transformationIndex++;
            }

            // record how many children the location had, and which offset in
            // this set of children was actually taken
            currNumOfChoices.add(transition.second
                .getParent()
                .getTransformationCount());
            currChosenIndices.add(transformationIndex);

            // record all nondeterministic scheduling decisions made during
            // execution of main transition body
            for (Iterator<IActionBacktrackingInfo> actions = tbi
                .getMainTransformationBacktrackingInfos()
                .iterator(); actions.hasNext();)
            {
                ISchedulingStrategyInfo ssi = actions
                    .next()
                    .getSchedulingStrategyInfo();

                for (int i = 0; i < ssi.getInfoCount(); i++)
                {
                    currNumOfChoices.add(ssi.getChoiceCount(i));
                    currChosenIndices.add(ssi.getChosenIndex(i));
                }
            }

            // next-state backtracking actions are defined not to be
            // nondeterministic, so we don't bother looking in them

            // record all nondeterministic scheduling decisions made to
            // facilitate model checking machinery (property automata, stateful
            // variables to implement optimizations, etc...)
            for (Iterator<IPostNextStateBacktrackingInfo> metadataActions = tbi
                .getPostNextStateBacktrackingInfos()
                .iterator(); metadataActions.hasNext();)
            {
                ISchedulingStrategyInfo ssi = metadataActions
                    .next()
                    .getSchedulingStrategyInfo();

                for (int i = 0; i < ssi.getInfoCount(); i++)
                {
                    currNumOfChoices.add(ssi.getChoiceCount(i));
                    currChosenIndices.add(ssi.getChosenIndex(i));
                }
            }

            // Now package up the scheduling info object for this transition

            result.add(new DefaultCounterExampleSchedulingInfo(
                "State-" + tbi.getStateId() + "-" + tbi.getInvisibleMoves(),
                tbi.getCanonicalThreadIndex(),
                currNumOfChoices.toArray(),
                currChosenIndices.toArray()));
        }

        return result;
    }

    protected void fillInitialVariableValues(
        IState vanillaState,
        IStateFactoryArguments args)
    {
        // Get bogus scheduling strategy context to use
        ISchedulingStrategyContext ssc = createContext(-1, -1, -1, vanillaState);
        ISchedulingStrategyInfo ssi = ss.newStrategyInfo();

        // Install the new context (none is yet installed)
        ee.setSchedulingStrategyContextInfo(ssc, ssi);

        // construct reverse (index --> name) globals identifier mapping
        IntObjectTable<String> globalNameMap = new IntObjectTable<String>();

        {
            for (String key : symbolTable.getGlobalIndexTable().keySet(true))
            {
                globalNameMap.put(
                    symbolTable.getGlobalIndexTable().get(key),
                    key);
            }
        }

        ArrayList<Type> globalTypes = symbolTable.getGlobalTypes();
        int globalsCount = globalTypes.size();
        IValue[] globalValues = new IValue[globalsCount];

        for (int i = 0; i < globalsCount; i++)
        {
            String name = globalNameMap.get(i);
            Global astNode = (Global) symbolTable.getIdentifierDefTable().get(
                name);
            Type globalType = globalTypes.get(i);

            if (astNode.getOptionalValue() != null)
            {
                InitialValue initVal = astNode.getOptionalValue();

                IValue newValue = ee.evaluate(ssc, initVal.getValue(), ssi);

                if (astNode.getOptionalValue().getOptionalCoercedType() != null)
                {
                    Type valueType = (Type) initVal.getValue().getProperty(
                        Exp.TYPE);
                    Type castType = (Type) initVal.getProperty(Exp.TYPE);

                    newValue = ee.evaluateCast(castType, valueType, newValue);
                }

                vanillaState.setGlobalValue(i, newValue);
            }
        }

        for (int tid : vanillaState.getThreadIds())
        {
            FSMSymbolTable fsmSymbolTable = symbolTable
                .getFSMSymbolTable(vanillaState.getLocation(tid));

            FSM fsm = fsmSymbolTable.getFSM();

            int argCount = fsm.getParamCount();
            int localCount = fsm.getLocalCount();

            for (int i = 0; i < localCount; i++)
            {
                Local astNode = fsm.getLocal(i);

                if (astNode.getOptionalValue() != null)
                {
                    InitialValue initVal = astNode.getOptionalValue();

                    IValue newValue = ee.evaluate(ssc, initVal.getValue(), ssi);

                    if (astNode.getOptionalValue().getOptionalCoercedType() != null)
                    {
                        Type valueType = (Type) initVal.getValue().getProperty(
                            Exp.TYPE);
                        Type castType = (Type) initVal.getProperty(Exp.TYPE);

                        newValue = ee.evaluateCast(
                            castType,
                            valueType,
                            newValue);
                    }

                    vanillaState.setLocalValue(tid, argCount + i, newValue);
                }
            }
        }

        // uninstall bogus scheduling context
        ee.unsetSchedulingStrategyContextInfo();
    }

    protected ArrayList<Pair<Integer, Transformation>> makeChoices(
        IntObjectTable<ArrayList<Transformation>> ets)
    {
        int[] keys = ets.keys();
        int size = keys.length;
        Arrays.sort(keys);

        ArrayList<Pair<Integer, Transformation>> result = new ArrayList<Pair<Integer, Transformation>>();

        for (int i = 0; i < size; i++)
        {
            int threadId = keys[i];

            for (Transformation t : ets.get(threadId))
            {
                result.add(new Pair<Integer, Transformation>(threadId, t));
            }
        }

        return result;
    }

    protected boolean shouldActivateThread(FSM fsm)
    {
        return fsm.getActive();
    }

    protected boolean shouldBacktrack()
    {
        ArrayList<ITransformationBacktrackingInfo> stack = sr
            .getBacktrackingInfos();

        if (stack.isEmpty())
        {
            // If no transition executed yet, then obviously not...
            return false;
        }
        else
        {
            ITransformationBacktrackingInfo lastTbi = stack
                .get(stack.size() - 1);

            IEndStateBacktrackingInfo endStateMarker = Util.findLast(
                lastTbi.getNextStateBacktrackingInfos(),
                IEndStateBacktrackingInfo.class);
            IExceptionBacktrackingInfo exceptionMarker = Util.findLast(
                lastTbi.getNextStateBacktrackingInfos(),
                IExceptionBacktrackingInfo.class);

            if (endStateMarker != null)
            {
                return true;
            }
            else if (exceptionMarker != null)
            {
                BogorException mce = exceptionMarker.getThrownException();

                if (mce instanceof AssertionBogorException)
                {
                    return true;
                }
                else if (mce instanceof RangeBogorException)
                {
                    return true;
                }
                else if (mce instanceof ExtFailedBogorException)
                {
                    return true;
                }
                else if (mce instanceof ExceptionThrownBogorException)
                {
                    return exceptionMarker.isUncaught();
                }
            }
        }

        return false;
    }

    protected void storeCounterExample(
        ArrayList<ITransformationBacktrackingInfo> backtrackingInfos,
        int stateId,
        int invisibleMoves,
        String reason)
    {
        ArrayList<ICounterExampleSchedulingInfo> info = extractErrorSchedule(backtrackingInfos);
        cew.storeCounterExample(info, reason);
    }

    // ~ Classes
    // ................................................................

    protected class MaxErrorReachedException
        extends RuntimeException
    {
        // ~ Constructors
        // .......................................................

        public MaxErrorReachedException()
        {
        }
    }

    protected class FoundValueException
        extends RuntimeException
    {
        // ~ Constructors
        // .......................................................

        public FoundValueException()
        {
        }
    }

    /**
     * @return a set of tuples whose first element says the name of the option,
     *         and whose second element says whether the option is required, and
     *         whose third element says whether the option is private to this
     *         module (and thus prefixed by the interface implemented, e.g.,
     *         <code>edu.ksu.cis.projects.bogor.module.ISearcher</code>) or
     *         global in scope (and thus no qualifier is prepended).
     */
    public Collection<Triple<String, Boolean, OptionScope>> getOptionIds()
    {
        ArrayList<Triple<String, Boolean, OptionScope>> result;
        result = new ArrayList<Triple<String, Boolean, OptionScope>>();

        for (String id : new String[]
            {
                PRINT_VERBOSE_TRACE_ID, WRITE_TRAIL_FILE_ID, PRINT_STATUS_ID,
                PRINT_COUNTER_EXAMPLES_ID, ALL_AS_ERRORS_ID, MAX_ERRORS_ID,
                MAX_DEPTH_ID, MAX_INVISIBLE_MOVES_ID,
                UPDATE_STATE_INCREMENT_ID, UPDATE_TRANSITION_INCREMENT_ID,
                INVARIANTS_ID, CHECK_BACKTRACK_ID
            })
        {
            result.add(new Triple<String, Boolean, OptionScope>(
                id,
                Boolean.FALSE,
                OptionScope.MODULE));
        }

        return result;
    }

    /**
     * @return a tuple whose first element says the domain of the option values,
     *         and whose second element says whether the option is multivalued
     *         (that is, a comma-separated list)
     */
    public Pair<Domain, Boolean> getOptionDomain(String id)
    {
        if (PRINT_VERBOSE_TRACE_ID.equals(id))
        {
            return new Pair<Domain, Boolean>(Domain.BOOLEAN, Boolean.FALSE);
        }
        else if (WRITE_TRAIL_FILE_ID.equals(id))
        {
            return new Pair<Domain, Boolean>(Domain.BOOLEAN, Boolean.FALSE);
        }
        else if (PRINT_STATUS_ID.equals(id))
        {
            return new Pair<Domain, Boolean>(Domain.BOOLEAN, Boolean.FALSE);
        }
        else if (PRINT_COUNTER_EXAMPLES_ID.equals(id))
        {
            return new Pair<Domain, Boolean>(Domain.BOOLEAN, Boolean.FALSE);
        }
        else if (ALL_AS_ERRORS_ID.equals(id))
        {
            return new Pair<Domain, Boolean>(Domain.BOOLEAN, Boolean.FALSE);
        }
        else if (CHECK_BACKTRACK_ID.equals(id))
        {
            return new Pair<Domain, Boolean>(Domain.BOOLEAN, Boolean.FALSE);
        }
        else if (MAX_ERRORS_ID.equals(id))
        {
            return new Pair<Domain, Boolean>(Domain.INT, Boolean.FALSE);
        }
        else if (MAX_DEPTH_ID.equals(id))
        {
            return new Pair<Domain, Boolean>(Domain.INT, Boolean.FALSE);
        }
        else if (MAX_INVISIBLE_MOVES_ID.equals(id))
        {
            return new Pair<Domain, Boolean>(Domain.INT, Boolean.FALSE);
        }
        else if (UPDATE_STATE_INCREMENT_ID.equals(id))
        {
            return new Pair<Domain, Boolean>(Domain.INT, Boolean.FALSE);
        }
        else if (UPDATE_TRANSITION_INCREMENT_ID.equals(id))
        {
            return new Pair<Domain, Boolean>(Domain.INT, Boolean.FALSE);
        }
        else if (INVARIANTS_ID.equals(id))
        {
            return new Pair<Domain, Boolean>(Domain.STRING, Boolean.TRUE);
        }
        else
        {
            return null;
        }
    }

    public Collection<String> getSuggestedValues(
        String id,
        IBogorConfiguration bc,
        SymbolTable st)
    {
        ArrayList<String> result = new ArrayList<String>();

        Pair<Domain, Boolean> domain = getOptionDomain(id);

        if (domain == null)
        {
            return result;
        }

        switch (domain.first)
        {
            case BOOLEAN:
                result.add(Boolean.toString(true));
                result.add(Boolean.toString(false));
                break;
            case INT:
                break;
            case STRING:
                if (INVARIANTS_ID.equals(id))
                {
                    Map<String, Type> funMap = st.getGlobalFunTable();

                    for (String funId : funMap.keySet())
                    {
                        Type type = funMap.get(funId);

                        if (!(type instanceof FunType))
                        {
                            continue;
                        }

                        FunType fType = (FunType) type;

                        if (fType.getParamTypeCount() == 0
                            && fType.getReturnType() instanceof BooleanType)
                        {
                            result.add(funId);
                        }
                    }
                }
                break;
            default:
                break;
        }

        return result;
    }

    /**
     * Checks whether the value of a configuration option is legal.
     * 
     * @param id
     *            the option's name, as returned by the first tuple element of
     *            an item returned by {@link #getOptionIds()}
     * @param value
     *            the value of the option, or <code>null</code> if unconfigued
     * @param st
     *            the symbol table for the BIR model
     * @param errors
     *            a container into which errors should be put. Implementors
     *            should not assume that <code>errors</code> is empty upon
     *            entry into this method; it may aggregate the results of
     *            calling <code>validate</code> on many
     *            <code>ISelfDescribingModule</code> instances.
     * @return <code>true</code> iff the option is supported and its value is
     *         legal
     */
    public boolean validate(
        String id,
        String value,
        IBogorConfiguration bc,
        SymbolTable st,
        Collection<FileMessage> errors)
    {
        Pair<Domain, Boolean> domain = getOptionDomain(id);

        // If the option is unknown, then call it a bad value
        if (domain == null)
        {
            return false;
        }

        // No option in this module is required, so a blank value
        // will be considered OK
        if (value == null)
        {
            return true;
        }

        switch (domain.first)
        {
            case BOOLEAN:
                if (!"true".equalsIgnoreCase(value)
                    && !"false".equalsIgnoreCase(value))
                {
                    errors.add(FileMessage.buildMessage(
                        "Expecting boolean",
                        new String[0]));
                    return false;
                }
                break;
            case INT:
                try
                {
                    int intValue = Integer.parseInt(value);

                    if (intValue < 0)
                    {
                        errors.add(FileMessage.buildMessage(
                            "Must be non-negative",
                            new String[0]));
                        return false;
                    }
                }
                catch (NumberFormatException nfe)
                {
                    errors.add(FileMessage.buildMessage(
                        "Expecting int",
                        new String[0]));
                    return false;
                }
                break;
            case STRING:
                if (INVARIANTS_ID.equals(id))
                {
                    int beginErrorCount = errors.size();

                    for (String funId : Util.splitCommaSeparatedList(value))
                    {
                        Map<String, Type> funMap = st.getGlobalFunTable();

                        Type type = funMap.get(funId);

                        if (!(type instanceof FunType))
                        {
                            errors.add(FileMessage.buildMessage(
                                "No such fun {0}",
                                new String[]
                                    {
                                        funId
                                    }));
                            continue;
                        }

                        FunType fType = (FunType) type;

                        if (fType.getParamTypeCount() != 0
                            || !(fType.getReturnType() instanceof BooleanType))
                        {
                            errors.add(FileMessage.buildMessage(
                                "Expected {0} to be boolean, zero-arity",
                                new String[]
                                    {
                                        funId
                                    }));
                        }
                    }

                    if (errors.size() != beginErrorCount)
                    {
                        return false;
                    }
                }
                break;
            default:
                break;
        }

        return true;
    }
}
